\begin{tabbing}
cr{-}antecedent\{i:l\}(${\it es}$;${\it Config}$;${\it Cmd}$;${\it Sys}$;$u$)($e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if\= csinput?(${\it Sys}$($e$))\+\+
\\[0ex]then $e$
\-\\[0ex]if ($u$($e$)) $\in_{b}$ ${\it Config}$ then prior(${\it Sys}$(valid))($u$($e$)) else $u$($e$) fi 
\-
\end{tabbing}